$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $h$:($T$$\rightarrow\mathbb{N}$).
\\[0ex]($\forall$$x$:$T$. ($f$($x$) = $x$) $\vee$ (($h$($f$($x$))) $<$ ($h$($x$))))
\\[0ex]$\Rightarrow$ ($\forall$$L$:($T$ List), $x$, $y$:$T$. $y$=$f$$\ast$($x$) via $L$ $\Rightarrow$ (($x$ = $y$) $\vee$ (($h$($y$)) $<$ ($h$($x$)))))